Nuprl Definition : grp_lt 13,42
a < b == a <(goset) b 
latex

clarification:

a <g b == a <(goset) b 
latex

Upgroups 1
Wellformedness Lemmasgrp lt wf
Definitionsa <p b, goset

origin